Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(filter,f),nil)  → nil
2:    app(app(filter,f),app(app(cons,y),ys))  → app(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))
3:    app(app(app(filtersub,true),f),app(app(cons,y),ys))  → app(app(cons,y),app(app(filter,f),ys))
4:    app(app(app(filtersub,false),f),app(app(cons,y),ys))  → app(app(filter,f),ys)
There are 9 dependency pairs:
5:    APP(app(filter,f),app(app(cons,y),ys))  → APP(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys))
6:    APP(app(filter,f),app(app(cons,y),ys))  → APP(app(filtersub,app(f,y)),f)
7:    APP(app(filter,f),app(app(cons,y),ys))  → APP(filtersub,app(f,y))
8:    APP(app(filter,f),app(app(cons,y),ys))  → APP(f,y)
9:    APP(app(app(filtersub,true),f),app(app(cons,y),ys))  → APP(app(cons,y),app(app(filter,f),ys))
10:    APP(app(app(filtersub,true),f),app(app(cons,y),ys))  → APP(app(filter,f),ys)
11:    APP(app(app(filtersub,true),f),app(app(cons,y),ys))  → APP(filter,f)
12:    APP(app(app(filtersub,false),f),app(app(cons,y),ys))  → APP(app(filter,f),ys)
13:    APP(app(app(filtersub,false),f),app(app(cons,y),ys))  → APP(filter,f)
The approximated dependency graph contains one SCC: {5,6,8,10,12}.
Tyrolean Termination Tool  (0.15 seconds)   ---  May 3, 2006